Nuprl Lemma : multiply_functionality_wrt_assoced
2,24
postcript
pdf
a
,
a'
,
b
,
b'
:
. (
a
~
a'
)
(
b
~
b'
)
((
a
b
) ~ (
a'
b'
))
latex
Definitions
a
~
b
,
P
Q
,
P
&
Q
,
Prop
,
b
|
a
,
x
:
A
.
B
(
x
)
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
divides
wf
origin
a, a', b, b':
. (a ~ a') 
(b ~ b') ((a
b) ~ (a'b')) a, a', b, b':. (a ~ a') (b ~ b') ((ab) ~ (a'b')) Qx:A. B(x)
T
x:A. B(x)